EPISTEMOLOGY, PROOF-CHECKING AND MATHEMATICAL THEORY OF COMPUTATION


	These three topics are being treated together in this proposal,
because they are being simultaneously advanced in a somewhat unified
effort.  This effort is based on a proof-checker for first order logic
called FOL that is being improved and extended by Richard Weyhrauch,
Bill Glassmire, Arthur Thomas and David Poole.

	Before describing the present state of this work and what is
planned in the next two years, it seems desirable to explain the
rationale of this effort, which is perhaps the Laboratory's major
effort in the theoretical side of artificial intelligence.


THE EPISTEMOLOGICAL PART OF ARTIFICIAL INTELLIGENCE

	Artificial intelligence has proved to be, as some people
expected and others didn't, a very difficult scientific subject.
In its first ten years, the limits of what could be done by
straightforward programming on specific intellectual problems
such as games and theorem proving were explored.  Besides that,
a number of ideas for general intelligent systems were also
explored with limited results.
It became clear that computer systems of human intelligence level
were not going to be obtained in one grand rush.  Once this is
understood, it becomes important to try to analyze the artificial
intelligence problem into a collection of subproblems and try
to split off subproblems that can be tackled separately and
whose solution will contribute to the solution of the problem
as a whole.  One such analysis (McCarthy and Hayes 1970) divides
the artificial intelligence problem into a heuristic part and
an epistemological part.

	The heuristic part of the problem was tackled first and
is best understood.